i:Id, ds:x:Id fp Type, da:k:Knd fp Type, x, y:Id, T1, T2:Type, ks1, ks2:(Knd List),
tr1:(k:{k:Knd| (k  ks1)} State(ds)Valtype(da;k)T1T1),
tr2:(k:{k:Knd| (k  ks2)} State(ds)Valtype(da;k)T2T2).
((x = y))
 ds || x : T1
 ds || y : T2
 R-state-var(i;ds;da;x;T1;ks1;tr1) || R-state-var(i;ds;da;y;T2;ks2;tr2) 

latex

Definitions	x:A. B(x), State(ds), P  Q, t  T, Top, S  T, suptype(S; T), x. t(x), P  Q, P  Q, P & Q, , x(s), State(ds)
Lemmas	ma-state-subtype, fpf-sub-join-left2, fpf-sub weakening, ma-valtype wf, fpf-compatible-join-cap, fpf-cap-single1, subtype rel self, fpf-cap wf, fpf-join wf, top wf, decl-state wf, fpf-compatible wf, Id wf, id-deq wf, fpf-single wf, not wf, Knd wf, l member wf, fpf wf